PRE_OP: A,B,C,D,E,F,U,V,W,X,Y,Z;
INF_PRED:=;
EQUALITY:=;
A=U∨A=V∨A=W;
B=U∨B=V∨B=W        ; 
C=U∨C=V∨C=W        ;
D=U∨D=V∨D=W        ;


¬A=B;
¬A=C;
¬A=D;


¬B=C;
¬B=D;


THM:C=D;;